\begin{tabbing}
$\forall$${\it es}$:ES, $a$:Atom1, $e$:E.
\\[0ex]$e$ sends $a$
\\[0ex]$\Rightarrow$ \=loc($e$) $>>$ $a$\+
\\[0ex]$\vee$ ($\exists$${\it e'}$:E. (${\it e'}$ $<$ $e$) \& ${\it e'}$ sends $a$ to loc($e$))
\\[0ex]$\vee$ (state when es{-}init(${\it es}$;$e$)):state@loc(es{-}init(${\it es}$;$e$))$>>$$a$
\-
\end{tabbing}